w-automaton(T;TA;M)
== :(b:Id(x:IdT(x))(?(TA(b))))
==  (:(k:Kndkindcase(k; a.TA(a); l,tg.M(l,tg) )(x:IdT(x))(x:IdT(x)))
==  (k:Kndkindcase(k; a.TA(a); l,tg.M(l,tg) )(x:IdT(x))
==  ((l:IdLnk  (t:Id  (M(l,t)))) List))) 

latex

---

clarification:

w-automaton(T;TA;M)
== :(b:Id(x:IdT(x))((TA(b)) + Unit))
==  (:(k:Kndkindcase(k; a.TA(a); l,tg.M(l,tg) )(x:IdT(x))(x:IdT(x)))
==  (k:Kndkindcase(k; a.TA(a); l,tg.M(l,tg) )(x:IdT(x))
==  ((l:IdLnk  (t:Id  (M(l,t)))) List))) 

latex

Definitions	, left + right, Unit, , Knd, kindcase(k; a.f(a); l,t.g(l;t) ), x:AB(x), type List, IdLnk, x:A  B(x), Id, f(a)
FDL editor aliases	w-automaton